// Copyright 2011 Google Inc. All Rights Reserved.
//
// Licensed under the Apache License, Version 2.0 (the "License");
// you may not use this file except in compliance with the License.
// You may obtain a copy of the License at
//
//     http://www.apache.org/licenses/LICENSE-2.0
//
// Unless required by applicable law or agreed to in writing, software
// distributed under the License is distributed on an "AS IS" BASIS,
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
// See the License for the specific language governing permissions and
// limitations under the License.

open util/ordering[State]

sig State {
  servers : set CapServer
}

abstract sig Transition {
 fromState : State,
 toState_ : State
 // the toState is fromState.next
} {
 toState_ = fromState.next
}

fun toState[trans : Transition] : State {
 trans.fromState.next
}

fact TransitionsOutOfStates {
 all s : State - last | one t : Transition | t.fromState = s
}

pred before[s1,s2:State] {
  s2 in s1.^next
}

/////////////////////////////////////////////////////////////////////

sig SendInvoke extends Transition {
  from: CapServer,
  to: CapServer,
  cap: Cap,
  args: set Cap
} {
  from in fromState.servers
  to in fromState.servers
  from != to
  cap.auth = to.auth
  some capSet:from.invokes[cap] | (cap + args) in capSet
  some to' : CapServer, m : Message {
    // This message didn't exist before
    not m in messages[fromState.servers] // TODO(jpolitz): Impact on sending same invoke twice?
    m.msgArgs = args

    // NOTE(jpolitz): If CapServer is extended, extra equality checks go here
    to'.impls = to.impls
    to'.auth = to.auth
    to'.caps = to.caps
    to'.type = to.type
    to'.recvBuf = to.recvBuf + (to.auth -> m)

    toState[this].servers = (fromState.servers - to) + to'
  }
}

sig BuggyInvoke extends Transition {
  from: CapServer,
  to: CapServer,
  cap: Cap,
  args: set Cap
} {
  from in fromState.servers
  to in fromState.servers
  from != to
  cap.auth = to.auth
  some capSet:from.invokes[cap] | (cap + args) in capSet
  some to' : CapServer, m : Message, c':from.caps - (cap + args) {
    // This message didn't exist before
    not m in messages[fromState.servers] // TODO(jpolitz): Impact on sending same invoke twice?
    // Here's the bug --- some extra cap is sent along with args
    m.msgArgs = args + c'

    // NOTE(jpolitz): If CapServer is extended, extra equality checks go here
    to'.impls = to.impls
    to'.auth = to.auth
    to'.caps = to.caps
    to'.type = to.type
    to'.recvBuf = to.recvBuf + (to.auth -> m)

    toState[this].servers = (fromState.servers - to) + to'
  }
}


sig SendResponse extends Transition {
  from: CapServer,
  to: CapServer,
  message: Message,
} {
  from in fromState.servers
  to in fromState.servers
  from != to
  some to', from':CapServer {
    // The message has been received by the sender of the response
    some (message & from.recvBuf[to.auth])
    
    from'.impls = from.impls
    from'.auth = from.auth
    from'.caps = from.caps + message.msgCap + message.msgArgs
    to'.type = to.type
    from'.recvBuf = from.recvBuf - (to.auth -> message)

    to'.impls = to.impls
    to'.auth = to.auth
    to'.caps = to.caps + (from.impls[message.msgCap.opaque][message.msgArgs])
    to'.type = to.type
    to'.recvBuf = to.recvBuf

    toState[this].servers = (fromState.servers - (to + from)) + from' + to'
  }
}

//run { some s:SendResponse | some s.args }

pred serverKnowsOpaque[o:Opaque, server:CapServer] {
  o = server.caps.opaque or some server.impls[o]
}

pred newOpaque[o:Opaque, s:State] {
  not serverKnowsOpaque[o, s.servers]
}

sig Grant extends Transition {
  server: CapServer,
  auth: Auth,
  opaque: Opaque,
  impl: set Cap ->set Cap
} {
  server in fromState.servers
  // The new cap is either brand new, or the capServer knew about it.
  // This models the unguessability of caps.  Note that auth is
  // unconstrained --- we assume that auths are well-known, so any
  // CapServer can grant a cap with any auth.
  newOpaque[opaque, fromState] or serverKnowsOpaque[opaque, server]
  some server' : CapServer, cap : Cap {
    cap.auth = auth
    cap.opaque = opaque
    server'.impls = server.impls + (opaque -> impl)
    server'.auth = server.auth
    server'.caps = server.caps + cap
    server'.type = server.type
    server'.recvBuf = server.recvBuf
    toState[this].servers = (fromState.servers - server) + server'
  }
}

pred serverGrantsNewOpaques[cs:CapServer] {
  all g:Grant | g.server.auth = cs.auth implies newOpaque[g.opaque, g.fromState]
}

//run { some g:Grant { g.opaque not in g.server.caps.opaque and no g.server.impls } } for 2 but 0 SendInvoke
pred testSendInvoke[i:SendInvoke] {
    some a: i.args { not a in i.to.caps }
    some i.to.impls[i.cap.opaque][i.args + i.to.caps]
}
//run testSendInvoke for 4 but 1 SendInvoke, 1 Message, 2 State

pred invokeAndResponse[inv:SendInvoke, resp:SendResponse] {
  no Wrappings.map
  some a1:inv.args | a1 not in inv.to.caps
  inv.to.auth = resp.from.auth
  inv.toState = resp.fromState
}
//run invokeAndResponse for 5 but 2 Auth, 0 Grant, 1 SendInvoke, 1 SendResponse, 3 State
/////////////////////////////////////////////////////////////////////

sig Cap {
  auth: Auth,
  opaque: disj Opaque
} 

sig Opaque { }
sig Auth { }

abstract sig CapServerT {}
one sig WrapServerT, NormalServerT extends CapServerT {}

sig CapServer {
  type: CapServerT,
  recvBuf: Auth -> Message,
  auth: Auth,
  caps: set Cap,
  // this capserver may invoke the LHS cap with the arguments on the RHS
  invokes: Cap -> set Cap,
  // for a given opaque and set of cap args, a specific set of caps is
  // specified
  impls: Opaque ->set Cap ->set Cap
}

fact {
  all cs:CapServer {
    all c:cs.invokes[Cap] | c in cs.caps
    cs.invokes.Cap in cs.caps
  }
}

fun messages[cs:CapServer]:set Message {
  { m:Message | m in cs.recvBuf[cs.auth] }
}

sig Message {
  msgArgs: set Cap,
  msgCap: Cap
} {
  // Messages don't float around, they are in at most one buffer in each state
  some cs:CapServer | this in messages[cs]
  all s:State, disj cs,cs':s.servers | this in messages[cs] implies not this in messages[cs']
  // Also, they all come from some kind of event
  some inv:SendInvoke | (not (this in messages[inv.fromState.*prev.servers])) and this in messages[inv.toState.servers]
}

//run { some Message }

fact capServersHaveUniqueAuthWithinState {
  all s:State, disj cs,cs':s.servers | cs.auth != cs'.auth
}

fact capServersExistInTime {
  all cs:CapServer | some s:State | cs in s.servers
}

fact implementationsLiveOnOneServerWithinState {
  all s:State, disj cs,cs':s.servers, o,o':Opaque | cs.impls[o] != cs'.impls[o']
}
fact implementationsReturnKnownCaps {
  all cs: CapServer, o:Opaque, c:Cap {
    cs.impls[o][c] in cs.caps
  }
}

// Not necessary or even always true, but a useful initial condition
pred noOverlappingOpaques[cs,cs':CapServer] {
  all o:Opaque | serverKnowsOpaque[o, cs] implies not serverKnowsOpaque[o, cs']
}

pred noOverlappingImpls[cs,cs':CapServer] {
  all o:Opaque | some cs.impls[o] implies no cs'.impls[o]
}

pred noOverlappingOpaquesGlobally[] {
  all disj cs,cs':CapServer | noOverlappingOpaques[cs,cs']
}

pred noOverlappingImplsGlobally[] {
  all disj cs,cs':CapServer | noOverlappingImpls[cs,cs']
}

//////////////////////////////////////////////////////////////////////

fun wrapServers[]:set CapServer {
  { v:CapServer | v.type = WrapServerT }
}

one sig Wrappings {
  map: Auth -> Auth
} {
  all w:wrapServers | some map[w.auth] and (not some a:map[w.auth] | a = w.auth)
  all w:CapServer - wrapServers | no map[w.auth]
}

pred wrapServersWrapArgs[] {
  all w:wrapServers {
    all argCaps:w.invokes.Cap {
      argCaps.auth = w.auth // arguments point back to this server
      // The opaque isn't one the client knows about
      all wrapped : { v:CapServer | v.auth = Wrappings.map[w.auth] and v in w.~servers.servers } {
        not serverKnowsOpaque[w.opaque, wrapped]
      }
    }
  }
}

fact wrapServersWrapReturns {
  all cs: Cap, ws: wrapServers, o:Opaque {
    let returns = ws.impls[o][cs] {
      // The cap points at the WrapServer
      returns.auth = ws.auth and
      // The opaque is not one the wrappee knows about 
      all wrapped : { v:CapServer | v.auth = Wrappings.map[ws.auth] and v in ws.~servers.servers } {
        not serverKnowsOpaque[returns.opaque, wrapped]
      }
    }
  }
}

assert wrapServerProtectsClient {
  all s:State - last {
    all disj wrapClient, ws : s.servers {
      ws in wrapServers and
      (all i:SendInvoke | i.from.auth = wrapClient.auth implies i.to.auth = ws.auth) and
      ws.auth != wrapClient.auth and
      (all other : {v : s.servers | v.auth not in ws.auth + wrapClient.auth } {
        noOverlappingOpaques[wrapClient, other]
      })
      implies
      let s' = s.next {
        all other' : {v : s'.servers | v.auth not in ws.auth + wrapClient.auth } {
          noOverlappingOpaques[wrapClient, other']
        }
      }
    }
  }
}

check wrapServerProtectsClient for 5 but 3 State, 3 Auth

assert maxInWrapper {
  all w:wrapServers | #(w.caps) < 4
}

check maxInWrapper for 3
